Search Results

Documents authored by Pagani, Michele

Document
DOI: 10.4230/LIPIcs.FSCD.2023.8
The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic

Authors: Thomas Ehrhard, Claudia Faggian, and Michele Pagani

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example of calculating the weighted relational semantics of a multiplicative proof-net improving runtime performance by storing intermediate results.
Cite as

Thomas Ehrhard, Claudia Faggian, and Michele Pagani. The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ehrhard_et_al:LIPIcs.FSCD.2023.8,
  author =	{Ehrhard, Thomas and Faggian, Claudia and Pagani, Michele},
  title =	{{The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.8},
  URN =		{urn:nbn:de:0030-drops-179926},
  doi =		{10.4230/LIPIcs.FSCD.2023.8},
  annote =	{Keywords: Linear Logic, Proof-Nets, Denotational Semantics, Probabilistic Programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.26
The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus

Authors: Simona Kašterović and Michele Pagani

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We consider the notion of probabilistic applicative bisimilarity (PAB), recently introduced as a behavioural equivalence over a probabilistic extension of the untyped lambda-calculus. Alberti, Dal Lago and Sangiorgi have shown that PAB is not fully abstract with respect to the context equivalence induced by the lazy call-by-name evaluation strategy. We prove that extending this calculus with a let-in operator allows for achieving the full abstraction. In particular, we recall Larsen and Skou’s testing language, which is known to correspond with PAB, and we prove that every test is representable by a context of our calculus.
Cite as

Simona Kašterović and Michele Pagani. The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kasterovic_et_al:LIPIcs.FSCD.2019.26,
  author =	{Ka\v{s}terovi\'{c}, Simona and Pagani, Michele},
  title =	{{The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.26},
  URN =		{urn:nbn:de:0030-drops-105338},
  doi =		{10.4230/LIPIcs.FSCD.2019.26},
  annote =	{Keywords: probabilistic lambda calculus, bisimulation, Howe’s technique, context equivalence, testing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.567
Modelling Coeffects in the Relational Semantics of Linear Logic

Authors: Flavien Breuvart and Michele Pagani

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Various typing system have been recently introduced giving a parametric version of the exponential modality of linear logic. The parameters are taken from a semi-ring, and allow to express coeffects - i.e. specific requirements of a program with respect to the environment (availability of a resource, some prerequisite of the input, etc.). We show that all these systems can be interpreted in the relational category (Rel) of sets and relations. This is possible because of the notion of multiplicity semi-ring and allowing a great variety of exponential comonads in Rel. The interpretation of a particular typing system corresponds then to give a suitable notion of stratification of the exponential comonad associated with the semi-ring parametrising the exponential modality.
Cite as

Flavien Breuvart and Michele Pagani. Modelling Coeffects in the Relational Semantics of Linear Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 567-581, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.CSL.2015.567,
  author =	{Breuvart, Flavien and Pagani, Michele},
  title =	{{Modelling Coeffects in the Relational Semantics of Linear Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{567--581},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.567},
  URN =		{urn:nbn:de:0030-drops-54384},
  doi =		{10.4230/LIPIcs.CSL.2015.567},
  annote =	{Keywords: relational semantics, bounded linear logic, lambda calculus}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.101
A characterization of the Taylor expansion of lambda-terms

Authors: Pierre Boudes, Fanny He, and Michele Pagani

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
The Taylor expansion of lambda-terms, as introduced by Ehrhard and Regnier, expresses a lambda-term as a series of multi-linear terms, called simple terms, which capture bounded computations. Normal forms of Taylor expansions give a notion of infinitary normal forms, refining the notion of Böhm trees in a quantitative setting. We give the algebraic conditions over a set of normal simple terms which characterize the property of being the normal form of the Taylor expansion of a lambda-term. From this full completeness result, we give further conditions which semantically describe normalizable and total lambda-terms.
Cite as

Pierre Boudes, Fanny He, and Michele Pagani. A characterization of the Taylor expansion of lambda-terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 101-115, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{boudes_et_al:LIPIcs.CSL.2013.101,
  author =	{Boudes, Pierre and He, Fanny and Pagani, Michele},
  title =	{{A characterization of the Taylor expansion of lambda-terms}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{101--115},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.101},
  URN =		{urn:nbn:de:0030-drops-41925},
  doi =		{10.4230/LIPIcs.CSL.2013.101},
  annote =	{Keywords: Lambda-Calculus, B\"{o}hm trees, Differential Lambda-Calculus, Linear Logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact